$\forall$$T$:Type, ${\it as}$, ${\it bs}$:($T$ List). rev(${\it as}$ @ ${\it bs}$) $\sim$ (rev(${\it bs}$) @ rev(${\it as}$))